/*
 * 
 */
package milecToMinisat;

import java.io.*;
import java.util.* ;

/** 
 * This class is an implementation of the interface ClauseGenerator 
 * 
 * @author ter-topcased-ups
 * @version 0.01, 2008/12/03
 * 
 */
public class ClauseGeneratorImpl implements ClauseGenerator {
	
	/** the converter use in this class for writing clauses */
	private static Converter myConverter = Converter.getInstance() ;
	
	private static ClauseGeneratorImpl instance ;
	
	/** a HashMap maintaining integer variables*/
	private HashMap<String,IntegerVariable> integerVariables ;
	
	/** the absolute path of minisat solver */
	private static String minisat ;
	
	public ClauseGeneratorImpl() {
		initialize() ;
	}
	
	private void initialize() {
		integerVariables = new HashMap<String,IntegerVariable>() ;
	}
	
	/**
	 * get an instance of ClauseGeneratorImpl
	 * @return the unique instance of ClauseGeneratorImpl
	 */
	// design singleton
	public static ClauseGeneratorImpl getInstance() {
		if (instance == null) {
			instance = new ClauseGeneratorImpl() ;
			}
		return instance ;
		}
	
	/**
	 * @return the minisat path
	 */
	public static String getMinisat() {
		return minisat;
	}

	/**
	 * @param minisat the minisat path to set
	 */
	public static void setMinisat(String newMinisat) {
		minisat = newMinisat;
	}

	public boolean checkModel() {
		try {
		File temporaryFile = File.createTempFile("autogenerated","opb") ;
		this.writeIn(temporaryFile) ;
		
		String[] commande = {minisat , temporaryFile.getAbsolutePath()} ;
		Process mySolver = Runtime.getRuntime().exec(commande) ;
		
		InputStream resultStream = mySolver.getInputStream() ;
		
		/*TODO interpreter le resultat
		 * cad : parser le retour de minisat et reconstruire valeurs depuis
		 * les tables de symboles locales.
		 */
		int sizeToRead = resultStream.available() ;
		byte[] result = new byte[sizeToRead] ;
		
		resultStream.read(result,0,sizeToRead) ;
		System.out.println(new String (result)) ;
		return true ;
		} catch (IOException ex) {
			System.err.println("temporary file can not be created") ;
	        System.err.println("Caught IOException: "   +  ex.getMessage());
	        return false ;
		} catch (SecurityException ex) {
			System.err.println("temporary file can not be created") ;
	        System.err.println("Caught SecurityException: "   +  ex.getMessage());
	        return false ;
		}
		
	}

	public IntegerVariable declareInteger(String name, int maximum) {
		if (integerVariables.containsKey(name)) {
			System.err.println("La variable `"+name+"`est deja declaree" 
					+ " (variableEntiere avec la borne  " 
					+	integerVariables.get(name).getBound()+":). ") ;
		} else {
			integerVariables.put(name, new IntegerVariable(name,maximum) ) ;
			myConverter.genIntegerConstraint(
					integerVariables.get(name),
					IntegerConstraintType.lessOrEqual,
					new IntegerCst(maximum) ) ;
		}
		return integerVariables.get(name) ;
	}
	
	public void addIntegerConstraint(IntegerExp exp,IntegerConstraintType constraintType ,IntegerCst cst)  {
		/*
		 * Premier jet : considere que exp est une variable
		 */
		if (exp.getClass() == IntegerVariable.class) {
			IntegerVariable intVar = (IntegerVariable)exp ;
			myConverter.genIntegerConstraint(intVar,constraintType, cst) ;
		}	else if (exp.getClass() == IntegerOperation.class ) {
			IntegerOperation intOp = (IntegerOperation) exp ;
			IntegerVariable tmp = addIntegerCalc(intOp) ;
			myConverter.genIntegerConstraint(tmp,constraintType, cst) ;
			//myConverter.genIntegerConstraint
		}
	}

	public IntegerVariable addIntegerCalc(IntegerOperation intOp) {
		IntegerVariable returnValue = IntegerVariable.tempVar(intOp.getSize()) ;
		IntegerExp finalLeft = intOp.getLeftSide() ;
		IntegerExp finalRight = intOp.getRightSide() ;
		if (finalLeft.getClass() == IntegerOperation.class ) {
			finalLeft = addIntegerCalc((IntegerOperation)finalLeft) ;
		}
		if (finalRight.getClass() == IntegerOperation.class) {
			finalRight = addIntegerCalc((IntegerOperation)finalRight) ;
		}
		
		myConverter.genIntegerCalc(intOp,finalLeft,finalRight,returnValue) ;
		return returnValue ;
	}

	public void writeIn(File aFile) throws IOException  {
		if (aFile != null &&  aFile.isFile() &&aFile.canWrite() ) {
			FileWriter myFileWriter = new FileWriter(aFile) ;
			
			myFileWriter.write(myConverter.getClauses()) ;
			myFileWriter.close() ;
		} else {
			if (aFile == null) {
				throw	new NullPointerException("aFile must not be null") ;
			}
			else if (! aFile.isFile()) {
				throw	new IllegalArgumentException ("aFile ("
						+aFile.getAbsolutePath()+")  is not a file") ; 
			}
				
		}
	}

}
